Annexe : Le type abstrait Vecteur

Lien Moodle : https://moodle.epita.fr/mod/page/view.php?id=108741

Contenu du cours

    types

        vecteur

    utilise

        entier, booléen, élément

    opérations

                 vect : entier x entier → vecteur
            modifième : vecteur x entier x élément → vecteur
                 ième : vecteur x entier → élément
        estinitialisé : vecteur x entier → booléen
             bornesup : vecteur → entier
             borneinf : vecteur → entier

    préconditions

        ième(v, i) est-défini-ssi borneinf(v) ≤ i ≤ bornesup(v) & estinitialisé(v, i) = vrai

    axiomes

        borneinf(v) ≤ i ≤ bornesup(v) ⇒ ième(modifième(v, i, e), i) = e
        borneinf(v) ≤ i ≤ bornesup(v) & borneinf(v) ≤ j ≤ bornesup(v) & i ≠ j
                        ⇒ ième(modifième(v, i, e), j) = ième(v, j)

        estinitialisé(vect(i,j),k) = Faux
        borneinf(v) ≤ i ≤ bornesup(v) ⇒ estinitialisé(modifième(v,i,e),i) = Vrai
        borneinf(v) ≤ i ≤ bornesup(v) & borneinf(v) ≤ j ≤ bornesup(v) & i ≠ j
                        ⇒ estinitialisé(modifième(v, i, e), j) = init(v, j)

        borneinf(vect(i, j)) = i
        borneinf(modifième(v, i, e)) = borneinf(v)

        bornesup(vect(i, j)) = j
        bornesup(modifième(v, i, e)) = bornesup(v)

    avec

        vecteur v
         entier i, j, k
        élément e